\begin{tabbing}
ecl{-}es{-}act(${\it es}$; $m$; $x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$ecl\_ind(\=$x$;\+
\\[0ex]$k$,${\it test}$.($\lambda$$e_{1}$,$e_{2}$. False);
\\[0ex]$a$,$b$,${\it aa}$,${\it ab}$.($\lambda$$e_{1}$,$e_{2}$. (${\it aa}$($e_{1}$,$e_{2}$))
\\[0ex]$\vee$ \=existse{-}between3(${\it es}$;$e_{1}$;$e_{2}$;$e$.(ecl{-}es{-}halt(${\it es}$; $a$)(0,$e_{1}$,es{-}pred(${\it es}$; $e$)))\+
\\[0ex]$\wedge$ (${\it ab}$($e$,$e_{2}$))));
\-\\[0ex]$a$,$b$,${\it aa}$,${\it ab}$.($\lambda$$e_{1}$,$e_{2}$. ((${\it aa}$($e_{1}$,$e_{2}$))
\\[0ex]$\wedge$ l{-}all(ecl{-}ex($b$); $n$.all$e$ from ${\it es}$ in [$e_{1}$;$e_{2}$).$\neg$(ecl{-}es{-}halt(${\it es}$; $b$)($n$,$e_{1}$,$e$))))
\\[0ex]$\vee$ \=((${\it ab}$($e_{1}$,$e_{2}$))\+
\\[0ex]$\wedge$ l{-}all(\=ecl{-}ex($a$); $n$.all$e$ from ${\it es}$ in [$e_{1}$;$e_{2}$).$\neg$(ecl{-}es{-}halt(${\it es}$; $a$)($n$,$e_{1}$,$e$))\+
\\[0ex])));
\-\-\\[0ex]$a$,$b$,${\it aa}$,${\it ab}$.($\lambda$$e_{1}$,$e_{2}$. ((${\it aa}$($e_{1}$,$e_{2}$))
\\[0ex]$\wedge$ l{-}all(\=cons(0; ecl{-}ex($b$));\+
\\[0ex]$n$.all$e$ from ${\it es}$ in [$e_{1}$;$e_{2}$).$\neg$(ecl{-}es{-}halt(${\it es}$; $b$)($n$,$e_{1}$,$e$))))
\-\\[0ex]$\vee$ \=((${\it ab}$($e_{1}$,$e_{2}$))\+
\\[0ex]$\wedge$ l{-}all(\=cons(0; ecl{-}ex($a$));\+
\\[0ex]$n$.all$e$ from ${\it es}$ in [$e_{1}$;$e_{2}$).$\neg$(ecl{-}es{-}halt(${\it es}$; $a$)($n$,$e_{1}$,$e$)))));
\-\-\\[0ex]$a$,${\it aa}$.($\lambda$$e_{1}$,$e_{2}$. es{-}pstar{-}q(${\it es}$;$x$,$y$.ecl{-}es{-}halt(${\it es}$; $a$)(0,$x$,$y$);$x$,$y$.\=${\it aa}$\+
\\[0ex]($x$
\\[0ex],$y$);$e_{1}$;$e_{2}$));
\-\\[0ex]$a$,$n$,${\it aa}$.if ($m$ =$_{0}$ $n$) then ecl{-}es{-}halt(${\it es}$; $a$)(0) else ${\it aa}$ fi ;
\\[0ex]$a$,$n$,${\it aa}$.${\it aa}$;
\\[0ex]$a$,$l$,${\it aa}$.${\it aa}$)
\-
\end{tabbing}